\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type).
\\[0ex]es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Leftarrow\!\Rightarrow$ guard(\=(($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex]((loc($e$) = $i$) $\vee$ ($\uparrow$es{-}isrcv(${\it es}$; $e$)))
\\[0ex]$\Rightarrow$ subtype\_rel(\=es{-}valtype(${\it es}$; $e$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; $e$); top)\+
\\[0ex]))))
\-\-\-
\end{tabbing}